{- 

    Copyright © 2011 - 2021, Ingo Wechsung
    All rights reserved.

    Redistribution and use in source and binary forms, with or
    without modification, are permitted provided that the following
    conditions are met:

        Redistributions of source code must retain the above copyright
        notice, this list of conditions and the following disclaimer.

        Redistributions in binary form must reproduce the above
        copyright notice, this list of conditions and the following
        disclaimer in the documentation and/or other materials provided
        with the distribution. Neither the name of the copyright holder
        nor the names of its contributors may be used to endorse or
        promote products derived from this software without specific
        prior written permission.

    THIS SOFTWARE IS PROVIDED BY THE
    COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR
    IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
    WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
    PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER
    OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
    SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
    LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF
    USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED
    AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING
    IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF
    THE POSSIBILITY OF SUCH DAMAGE.

                                                                 -}

{--
 *
 * This code is inspired by the type checker found in the 2004 version of the paper
 * _Practical type inference for arbitrary-rank types_ by Simon Peyton Jones.
 *
 * In addition to higher ranked polymorphism for the full frege language,
 * the type checker also
 *  - does kind checking and inference
 *  - infers and checks type class constraints
 *  - does type directed name resolution for expressions @x.m@ where _x_
 *    is an expression and _m_ is a name, that is resolved relative to the type of _x_
 *    (think field labels)
 *  - resolved overloaded native methods
 *  - checks sanity of native functions types with regards to mutability 
 *
 * In contrast to earlier Frege versions, I gave up quantifying
 * un-annotated local let bindings.
 * For a rationale see the paper /Let Should Not Be Generalised/
 * ("http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/let-gen.pdf")

 * It is possible to obtain a quantified type by writing annotations for
 * local bindings. However, often when a quantified type is possible, no references
 * to other local bindings exist, in which case the local binding will have been lifted
 * to the top level. This is entirely transparent for the user, there is no way to
 * tell if a local binding has been lifted except by looking at the trace or the
 * generated java code.
 *
 *
 * Requirements to obey:
 *  - 'tcRho' (which is invoked by 'checkRho' and 'inferRho') must ultimately call 'instRho'
 *  - the expression passed to 'tcRho' et al. must be replaced by the resulting expression.
 *
 * This will ensure the following invariant:
 *  - The result of 'tcRho' is an 'Expr', whose 'Expr.typ' 'isJust'. The expression
 *    passed to tcRho is invalid and must not be used anymore.
 -}

package frege.compiler.Typecheck where

import frege.Prelude hiding(<+>)
import Data.TreeMap as TM(TreeMap, values, lookup, insert,  
                        each, keys, including, union, contains)
import Data.Graph (stronglyConnectedComponents tsort)
import Data.List(groupBy, sortBy)

import Compiler.enums.Flags as Compilerflags(flagSet, OVERLOADING, TRACEO, TRACET, TRACEZ)
import Compiler.enums.TokenID
import Compiler.enums.Visibility
import Compiler.enums.SymState
import Compiler.enums.Literals

import  Compiler.types.Positions
import  Compiler.types.Tokens
import  Compiler.types.Packs
import  Compiler.types.QNames
import  Compiler.types.Types
import  Compiler.types.Patterns as P
import  Compiler.types.Expression
import  Compiler.types.Symbols
import  Compiler.types.Global as G

import  Compiler.common.Errors as E()
import  Compiler.common.Types  as TH
import  Compiler.common.Resolve as R(weUse)
import  Compiler.common.SymbolTable
import  Compiler.common.Binders(avoidBinders)

import  Compiler.classes.Nice

import  Compiler.instances.Nicer

import Lib.PP(text, msgdoc, nest, stack, <>, </>, <+/>, <+>)
import frege.compiler.Utilities     as U(findC, findD, findV, findVD, symVD, freeTVars, freeTVnames,
                                            mapEx, foldEx, arity)
import frege.compiler.Kinds         as K()                                            

import frege.compiler.tc.Util
-- import frege.compiler.Javatypes
import frege.compiler.tc.Methods    as M()
import frege.compiler.tc.Patterns


post = stio true

--- construct a tree of all our member functions
memberTree = do
    g <- getST
    let envs = g.thisTab : [ Symbol.env sy | sy <- values g.thisTab, Symbol.{env?} sy ]
        mems = fold ins empty [ sy | env <- envs, sy@SymV {name=MName _ _} <- values env, g.ourSym sy]
        ins :: TreeMap String [Symbol] -> Symbol -> TreeMap String [Symbol]
        ins t sy
            | Just list <- t.lookup b = if sy `elem` list then t else  t.insert b (sy:list)
            | otherwise = insert b [sy] t
            where b = (Symbol.name sy).base
    stio mems

fundep mtree (SymV {name, expr=Just dx})  = do
    g <- getST
    deptree <- dx >>= U.ourGlobalFuns mtree
    let dep = [ Symbol.name sy | sy <- keys deptree, g.ourSym sy,
                    -- leave annotated symbols and symbols with sigmas out
                    sy.{expr?} && isPSigma sy.typ || not sy.{expr?}   ]
    stio (name, dep)
fundep mtree (SymV {name, expr=Nothing}) = stio (name, [])
fundep mtree other = do
    g <- getST
    E.fatal other.pos (text ("fundep: strange symbol: " ++ other.nice g))


--- collect all variable symbols and their dependencies
pass = do
    names <- liftStG do
        E.logmsg TRACET Position.null (text "start type check pass")
        changeST Global.{tySubst=empty}
        mtree <- memberTree
        g <- getST
        let ourvars = U.allourvars g

        mapSt (fundep mtree) ourvars

    let groups = tsort names

    liftStG do
        g <- getST
        E.logmsg TRACET Position.null (text  ("names: " ++ joined " " (map (flip QName.nice g • fst) names)))
        E.logmsg TRACET Position.null (text ("groups: " ++ display (map (map (flip QName.nice g)) groups)))

        annotateMain

    forsome groups (liftStG . checkgroup)

    liftStG do
        g <- getST
        when (g.errors == 0) do
            checkMain      -- look if there is a main function and check if the type is ok

        changeST Global.{sub <- SubSt.{resErrors = 0}}  -- so that subsequent passes do not run accidentally
    
        unusedImports
    
    return ("functions", length names)

--- e.g. @tc "Int"@ is the 'Tau' with type constructor for @PreludeBase.Int@
tc n = TCon {pos=Position.null, name=TName pPreludeBase n}

mainSigmaA t = ForAll [] 
                (RhoFun [] (ForAll [] (RhoTau [] strings)) 
                           (RhoTau [] iovoid))
    where
        strings = TApp (tc "[]") tauString          -- [String]
        iovoid = TApp (TApp (tc "ST") (tc "RealWorld")) t

mainSigma = ForAll [] 
                (RhoFun [] (ForAll [] (RhoTau [] strings)) 
                           (RhoTau [] iovoid))
    where
        strings = TApp (tc "[]") tauString          -- [String]
        iovoid = TApp (TApp (tc "ST") (tc "RealWorld")) (tc "()")

mainSimple (ForAll xs RhoFun{rho}) = ForAll xs rho
mainSimple sigma = sigma

{--
 * make sure that, for example,  @main _ = return ()@ is not rejected later because of
 * inferred type @forall a m Monad m . a -> m ()@
 
 Note that code like:
 
 > main = return
 
 is bound to fail, because it gets annotated as
 
 > main :: IO ()
 -}
annotateMain = do
    g <- getST
    case g.findit (VName g.thisPack "main") of
        Just sym | sym.name.pack == g.thisPack,
                   Just dx <- sym.expr,
                   not sym.anno = do
                        x <- dx 
                        if U.lambdaDepth x > 0 
                            then changeSym sym.{typ = mainSigma, anno = true}
                            else changeSym sym.{typ = mainSimple mainSigma, anno = true}
        _ -> stio ()

checkMain = do
    g <- getST
    tau <- Util.newMeta2 ("a", KType)
    case g.findit (VName g.thisPack "main") of
        Just sym | sym.name.pack == g.thisPack -> do
            let m = Vbl {pos = sym.pos, name = sym.name, typ = Just pSigma}
                sigma 
                    | RhoFun{} <- sym.typ.rho = mainSigmaA tau 
                    | otherwise               = mainSimple (mainSigmaA tau)
            checkAnnotated m sigma
            gnew <- getST
            when (g.errors < gnew.errors) do
                E.error sym.pos (msgdoc ("The main function must have type " ++ nicer sigma g))
            when (g.errors == gnew.errors && not (null sym.typ.rho.context)) do
                E.error sym.pos (msgdoc ("The main function type must not have type class constraints."))
        _ -> stio ()
-- type check one group after the other as long as there are fewer than 7 errors
-- checkgroups [] = stio ()
-- checkgroups (g1:gs) = do
--     g <- getST
--     cancel <- doio g.sub.cancelled
--     when (not cancel && g.errors < 7) do
--         
--         -- E.logmsg TRACET Position.null (text ("typechecking group: " ++ joined " " (map (flip QName.nice g) g1)))
--         checkgroup  g1
--         checkgroups gs

{-- 
    We continue type checking only as long as we have less than 7 errors.
    The reason is that a type error may trigger a lot of follow up errors
    that may obscure the true origin.
    
    Experience shows that the _first_ few error messages are the best,
    yet not all programmers seem to know this.
    
    Yet, we must continue with local definitions, or otherwise
    we encounter untyped expressions later.
    
    -}
checkgroup  nms = do
    g <- getST
    when (g.errors < 7 || length g.typEnv > 0) (checkgroup7 nms)

--- Type check a group of top level functions that depend on each other.        
checkgroup7 nms = do
    g <- getST
    E.logmsg TRACEZ Position.null (text ("typechecking group: " ++ joined " " (map (flip QName.nice g) nms)))
    unless (null g.typEnv) do
        mapSt findV nms >>= mapM_ renameSigma
    -- we set up typEnv with the names of the group members so that 'envTvs' will find them
    changeST Global.{typEnv <- (nms ++)}

    -- with Nil do
        -- sequence_ enterChecked
        -- foreach syms (\sym -> U.linkq (Local (show (Symbol.sid sym))) sym)
    -- foreach nms verbose
    foreach nms checkName
    syms <- mapSt findV nms
    when (length syms > 1 || any ((==Recursive) • Symbol.state) syms)
            (foreach nms checkName)
    changeST Global.{typEnv <- drop (length nms)}
    g <- getST
    -- foreach nms verbose
    when (length g.typEnv == 0)  do
        quantifyMany nms
    -- DO NOT quantify let
    -- when (length g.typEnv > 0 && length nms == 1) do
    --     quantifyOne nms
    foreach nms verbose
    foreach nms typeSanity 
    g <- getST
    when (g.errors == 0 && length g.typEnv == 0) (foreach nms substInstMethod)
    -- changeST Global.{checking=g.checking}
  where
    verbose nm = do
        g <- getST
        sym <- findV nm
        let sig = Symbol.typ sym
        E.explain (Symbol.pos sym) (text (sym.nice g ++ " :: " ++ sig.nicer g))
    typeSanity nm = do
        sym <- findV nm
        sym <- checkKind sym
        checkAmbiguous sym sym.typ
        checkReturn    sym sym.typ
        -- sym <- removeCheckedCtx sym sym.typ
        case sym.name of
            Local{} -> return ()
            aGlobalName -> do       -- issue #23
                    -- there is no way a local function can have constraints:
                    -- Either the constraint is of the form C (T x), then it was checked and discharged
                    -- Or, it is of the form C a, then it is passed upwards
                    -- Or, it used to be of the form C t1234 and t1234 was substituted meanwhile.
                    -- Hence, all constraints on local functions must be removed
                    case sym.expr of
                        Nothing -> return ()
                        Just dx   -> do
                            x  <- dx
                            ex <- U.mapEx false removeCtx x
                            changeSym sym.{expr = Just (return ex)} 
              where
                    scrapCtx it = do
                        let sig = (Symbol.typ it).{rho <- clear}
                            clear ∷ Rho → Rho
                            clear RhoFun{context, sigma, rho} = RhoFun{context=[], sigma, rho = clear rho}
                            clear RhoTau{context, tau} = RhoTau{context=[], tau}
                        nex <- case it.expr of
                            Just x  -> x >>= U.mapEx false removeCtx >>= (return . Just . return)
                            Nothing -> return Nothing
                        changeSym it.{typ=sig, expr = nex}
                    removeCtx (it@Let{env}) = do
                        syms <- mapM U.findV env
                        foreach syms scrapCtx
                        return (Left it)
                    removeCtx x = return (Left x)

checkKind ∷ Symbol → StG Symbol
checkKind sym = correctK empty sym
  where
    correctK ∷ TreeMap String Tau → Symbol → StG Symbol
    correctK subst (sym@SymV{typ,expr}) = do
        --g ← getST
        --E.logmsg TRACEZ sym.pos (text "Checking kind of" <+> text (nice sym g))
        sig     ← bool
                    (pure typ) 
                    (fst <$> K.kiSigma [] [] typ)
                    (null typ.bound)
        let rsubst = sig.extendEnv subst -- (zip sig.vars (sig.tvars sym.pos))
        ex      ← maybe
                    (pure Nothing)
                    (\x → Just <$> (x >>= mapEx false (correctKind rsubst)))
                    expr
        let new = sym.{typ=sig, expr = fmap pure ex}
        return new
    correctK subst sym = error "only SymV allowed" 

    correctKind subst Let{env, ex, typ} = do
        syms    ← mapM U.findV env
        mapM_ (correctK subst) syms
        ex'     ←  mapEx false (correctKind subst) ex
        pure $ Right Let{env, ex = ex', typ = fmap (substSigma subst) typ }
    correctKind subst x = pure $ Left  x.{typ ← fmap (substSigma subst)}

checkAmbiguous sym (ForAll bnd r) = do
        let ra = r.{context=[]}                     -- ctx => rho    --> rho
            rb = (rhoInt).{context=r.context}       -- Int           --> ctx => Int
            va = freeTVnames [] ra
            vb = freeTVnames [] rb
            bad = filter (`notElem` va) vb
        if null bad then stio ()
          else do
            g <- getST
            E.error (Symbol.pos sym) (msgdoc ("Ambiguous type "
                    ++ nicer r g ++ " in " ++ nice sym g))
            E.hint  (Symbol.pos sym) (msgdoc ("It is not clear at what types to instantiate "
                    ++ (if length bad == 1 then "type variable " else "type variables ")
                    ++ joined ", " bad ++ " that "
                    ++ (if length bad == 1 then "occurs" else "occur")
                    ++ " in the context, but not in the type."))
            E.hint  (Symbol.pos sym) (msgdoc ("This can happen through constructs like (Enum.ord • Enum.from) "
                    ++ " where a class context is both introduced and eliminated locally so "
                    ++ "that a caller can not know which type is meant."))

checkReturn :: Symbol -> Sigma -> StG ()
checkReturn sym sigma =
    case U.returnType sigma.rho of
        (_, []) -> stio ()
        (t, ss) -> do
            let svars = [ v | ForAll bs br <- ss, v <- U.freeTVnames (map _.var bs) br ]
                        ++ keys (U.freeCtxTVars [] empty sigma.rho.context)
                tvars = case t of
                    TVar {pos} -> [t.var]
                    TApp _ _ | (TVar {var}:_) <- t.flat = [var]
                    _ -> []
            if all (`elem` svars) tvars then stio ()
              else do
                g <- getST
                U.symWarning E.warn sym (msgdoc ("application of " ++ sym.name.nice g ++ " will diverge."))
{-
removeCheckedCtx :: Symbol -> Sigma -> StG Symbol
removeCheckedCtx sym sigma
    | any Context.checked sigma.rho.context = do
        let new = sym.{typ = sigma.{rho <- Rho.{context <- filter (not • Context.checked)}}}
        U.changeSym new
        stio new 
    | otherwise = stio sym
-}

resolveConstraints :: Symbol -> StG ()
resolveConstraints sym
    | SymV{typ, expr=Just x, anno=false, state} <- sym, state != Recursive = do
        x   <- x >>= resolveHas 
        cxs <- collectConstrs x
        rho <- simplify sym.pos typ.rho.{context=cxs}
                >>= simplify sym.pos        -- remove duplicates 
        -- Drop the contexts that contain a rigid tvar that is not occurring in the type itself.
        -- Those stem from typechecking applications of higher rank functions where
        -- there is a constraint in an inner forall.
        -- The rigid context remains intact on the application itself, which will help us
        -- in code generation to identify them.
        g <- getST
        let rhometas = rhoTvs g rho.{context=[]}
            ctxmetas = map (ctxTvs g) rho.context
        let filteredCtx = [ ctx | (metas, ctx) <- zip ctxmetas rho.context,
                                  all (`elem` rhometas)  (filter (not . MetaTv.isFlexi) metas)]
        changeSym sym.{typ <- Sigma.{rho <- rmtrailing . Rho.{context=filteredCtx}}, 
                         expr = Just (return x)}
    | otherwise = return ()
    where 
        rmtrailing rho 
            | RhoFun{} <- rho = rho.{rho <- zapctx}
            | otherwise = rho
        zapctx RhoTau{context, tau} = RhoTau{context=[], tau}
        zapctx RhoFun{context, sigma, rho} = RhoFun{context=[], sigma, rho = zapctx rho} 
     
{--
 * look for applications of class member functions in the code of the named item
 * and replace them with instance member functions, if possible.
 *
 -}
substInstMethod :: QName -> StG ()
substInstMethod qname = do
        g <- getST
        -- when (U.isOn g.options.flags OPTIMIZE) do
        sym <- findV qname
        case sym.expr of
            Nothing -> stio ()
            Just dx -> do
                x <- dx
                x <- mapEx true substInst x
                changeSym sym.{expr = Just (return x)}

--- replace class member with instance member, if possible
substInst (vbl@Vbl {pos, name = MName tn bs, typ = Just (ForAll [] rho)})
        -- check if vbl is instaniated to tn
    | [ctx@Ctx {cname, tau=ctau}] <- filter ((==tn) • Context.cname) rho.context
    = do
        g <- getST
        let tau = reducedTau g ctau
        case instTauSym tau g of
            Just symt -> do           -- we have a type name
                symc <- findC tn      -- must be a class because it appears in a contexts cname
                case filter ((symt.name ==) • fst) symc.insts of    -- find instance
                    [] -> E.fatal pos (text (symc.nice g ++ " has no instance for " ++ symt.nice g))
                    [(_,iname)]
                        {- | MName iname bs != qname -} -> do
                            mem  <- findV vbl.name
                            case g.findit (MName iname bs) of
                                Just imem -> do 
                                    let nrho = rho.{context <- filter (not • sameCtx ctx)}
                                        strho = substRho 
                                                    (unifySigma g imem.typ ForAll{bound=[], rho=nrho}) 
                                                    imem.typ.rho
                                        !repl | SymV{} <- imem = vbl.{name=imem.name, 
                                                                        typ = Just (ForAll [] strho)}
                                              | SymD{} <- imem = Con{pos=vbl.pos, 
                                                                        name=imem.name, 
                                                                        typ = Just (ForAll [] strho)}
                                              | otherwise = error ("substInst WTF??? : " ++ nicer imem g) 
                                    E.logmsg TRACEO pos (
                                        text ("replace " ++ vbl.name.nice g) 
                                        </> nest 4 (
                                            text (":: " ++ vbl.typ.nicer g)
                                            </> text ("sigma :: " ++ mem.typ.nicer g) 
                                            </> text ("with  " ++ imem.name.nice g)
                                            <+> text (" :: " ++ imem.typ.nicer g)
                                            </> text ("@@ " ++ nrho.nicer g)
                                            </> text ("?? " ++ strho.nicer g)))
                                    changeST Global.{sub <- SubSt.{
                                        idKind <- insert (KeyTk vbl.pos.first) (Right imem.name)}}
                                    weUse imem.name
                                    stio (Left repl)
                                Nothing -> E.fatal vbl.pos (msgdoc ("substInst: trying "
                                            ++ nice vbl g ++ ", but  "
                                            ++ nice (MName iname bs) g
                                            ++ " does not exist!"))
                        -- | otherwise = do
                        --     E.logmsg TRACEO pos (text ("mustn't substitute " ++ qname.nice g ++ " in its own body."))
                        --     stio (Left vbl)
                    _ -> E.fatal pos (text (symc.nice g ++ " has multiple instances for " ++ symt.nice g))
            _ -> do
                E.logmsg TRACEO pos (text ("no suitable instance: " ++ vbl.nice g ++ " :: " ++ rho.nicer g))
                stio (Left vbl)        -- TVar or Meta
    | otherwise = do
        g <- getST
        E.logmsg TRACEO pos (text ("no suitable constraint: " ++ vbl.nice g ++ " :: " ++ rho.nicer g))
        stio (Left vbl)
--- Also, make sure no DWIM literal has a constraint in its type.
substInst (lit@Lit{pos, kind, value, typ=Just (ForAll [] rho)})
    | kind == LInt || kind == LDouble,
      not (null rho.context) = pure (Right lit.{typ=Just (ForAll [] rho.{context=[]})})
substInst x = stio (Left x)

renameSigma ∷ Symbol -> StG ()
renameSigma sym | sym.name.isLocal && sym.anno = do
    g   ← getST
    outer ← mapSt findV g.typEnv
    let avoid  = \c → c `elem` concatMap (Sigma.vars . Symbol.typ) outer 
                    || (any (null . Sigma.vars . Symbol.typ) outer && avoidBinders g c)
        newsym = sym.{typ ← avoidSigma avoid }
    when (sym.typ.vars != newsym.typ.vars) do
        E.warn sym.pos ((text "Renamed type variables in annotated type of let bound function "
                            <+> text sym.name.base) 
                            </> (text "was: " <+> text (sym.typ.nicer g))
                            </> (text "now: " <+> text (newsym.typ.nicer g))
                            </> text "because of (potential) type variable naming conflicts.")
        changeSym newsym
    pure ()
renameSigma other = pure ()


checkName nm = do
    g       <- getST
    sym     <- findV nm
    -- sym     <- if nm.isLocal && sym.anno then renameSigma sym else pure sym
    E.logmsg TRACEZ sym.pos (text ("checkName:  " ++ sym.name.nice g ++ " :: " ++ sym.typ.nice g))
    -- E.logmsg TRACET sym.pos (text ("checkName:  " ++ sym.name.nice g ++ " :: " ++ sym.typ.nice g))
    sigma   <- checkSym sym
    unless (nm.isLocal) do
        sym     <- findV nm
        resolveConstraints sym
  where
    checkSym sym = do
        g <- getST
        -- E.logmsg TRACEZ (Symbol.pos sym) (text ("typechecking " ++ sym.nice g ++ ", state=" ++ show sym.state))
        -- E.logmsg TRACET (Symbol.pos sym) (text ("typechecking " ++ sym.nice g ++ ", state=" ++ show sym.state))
        case sym of
            SymV {nativ = Just _, typ = t} | not (isPSigma t) -> do
                (sig, _) <- K.kiSigma [] [] t
                E.logmsg TRACEZ sym.pos (text "after kind inference: " <+> 
                    text (sig.nicer g)) 
                changeSym sym.{typ=sig}
                M.sanity sym.{typ=sig}
                return sig
            SymV {expr = Nothing, name, pos, typ = t}
                | not (isPSigma t),
                  MName c _ <- name,
                  Just (SymC {pos}) <- g.findit c = do
                    (sig, _) <- K.kiSigma [] [] t
                    changeSym sym.{state=Typechecked, vis=Abstract, typ = sig}
                    stio t
                | otherwise = do
                    E.error pos (msgdoc ("implementation missing for " ++ sym.nice g))
                    (sig, _) <- K.kiSigma [] [] t
                    changeSym sym.{state=Typechecked, typ=sig}
                    stio t
            SymV {expr = Just dx, typ = t}
                | isPSigma t,
                  sym.state `elem` [Unchecked, Typechecking, Recursive] = do
                    x <- dx
                    rho0 <- approxRho x 
                    ex <- case rho0 of
                        RhoTau{} -> do
                            changeSym sym.{state=Typechecking}
                            (rho, ex) <- inferRho x  -- CAF ?
                            return ex
                        RhoFun{} -> do
                            changeSym sym.{state=Typechecking, typ = ForAll [] rho0}
                            checkRho x rho0
                    sym <- findV sym.name       -- refresh, might be updated meanwhile
                    let newstate = if sym.state != Recursive then Typechecked else Recursive
                    newsig <- maybe (error "untyped after checkRho") pure ex.typ
                    changeSym sym.{typ = newsig, expr=Just (return ex), state = newstate}
                    stio newsig
                    
            SymV {expr = Just dx, typ = t, state, anno}
                | not (isPSigma t), state == Unchecked  = do
                    x <- dx
                    (sig, _) <- K.kiSigma [] [] t
                    E.logmsg TRACEZ sym.pos (text "checkName: annotation after kind inference:" 
                        <+> text (nice sig g))
                    x <- checkAnnotated x sig
                    -- t <- canonicSignature t
                    changeSym sym.{state = Typechecked, expr = Just (return x), typ = sig }
                    stio sig
                | not (isPSigma t), state == Typechecked && anno = stio t     -- opt: do not recheck annotated
                | not (isPSigma t), state == Recursive || state == Typechecked = do
                    x <- dx
                    (rho, ex) <- inferRho x
                    rho <- zonkRho rho
                    sym <- findV sym.name       -- refresh, might be updated meanwhile
                    let newsig   = ForAll [] rho
                    changeSym sym.{typ = newsig, expr=Just (return ex), state = Typechecked}
                    stio newsig
            wrongsy -> E.fatal wrongsy.pos (text ("checkSym: wrong symbol: " ++ wrongsy.nice g
                ++ ", state=" ++ show wrongsy.state
                ++ ", expr isJust: " ++ show (isJust wrongsy.expr)
                ++ ", typ : " ++ wrongsy.typ.nice g))

quantifyOne nms = do
        g <- getST
        sym <- U.findV (head nms)
        lsyms <- mapSt U.findV g.typEnv
        let rec = [ Symbol.typ sym | sym <- lsyms,
                                    sym <- (g.follow sym),    -- follow aliases
                                    Symbol.state sym == Recursive]
        when (false && null sym.typ.rho.context && not (TH.isFun sym.typ g) && null rec) do
            quantifyWith (quantifiedExcept sym.sid) nms
        stio ()

quantifyMany = quantifyWith quantified
quantifyWith f nms = do
        syms <- mapSt findV nms     -- unquantified symbols
        g <- getST
        unless (null syms) do
            E.logmsg TRACET (head syms).pos (text ("quantify " ++ joined ", " (map (flip QName.nice g) nms)))
            E.explain       (head syms).pos (msgdoc ("quantify " ++ joined ", " (map (flip QName.nice g) nms)))
            -- foreach syms logty
        let qsyms = [ (name, rho) | (sy@SymV {name, expr  = Just _,
                                     nativ = Nothing,
                                     anno  = false,
                                     typ   = (ForAll [] rho)}) <- syms, not (isPSigma sy.typ)]
            asyms = [ (name, typ) | sy@SymV {name, expr  = Just _,
                                     nativ = Nothing,
                                     anno  = true, typ} <- syms ]
            -- sigRho (ForAll [] rho) = rho
            rhos = map snd qsyms
            qnms = map fst qsyms
        sigs <- f rhos
        foreach (zip qnms sigs) changeSig
        foreach asyms changeSig
    where
        changeSig (qnm, sigm) = do
            sym <- findV qnm
            case sym of
                SymV {expr = Just dx} -> do
                    x <- dx
                    zex <- zonkExpr x           -- from here on no bound Meta anywhere
                    zex <- zonkRigid (Sigma.vars sigm) zex    -- replace Rigid#nnn a where a is bound
                    let sigma = substRigidSigma (Sigma.vars sigm) sigm
                    changeSym sym.{typ = sigma, expr = Just (return zex), anno = true}
                    g <- getST
                    E.logmsg TRACET (Symbol.pos sym) (text ("qfy: " ++ sym.nice g ++ " :: " ++ sigma.nice g))
                    E.explain (Symbol.pos sym) (text (sym.nice g ++ " :: " ++ sigma.nicer g))
                other = Prelude.error "findV behaves badly"


-- zonkRigid []    ex = stio ex
zonkRigid :: [String] -> Expr -> StG Expr
zonkRigid bound ex = do
        -- g <- getST
        mapEx false zonk ex
    where
        symWork (symv@ SymV {pos, expr, typ = sig}) = do
                        g <- getST
                        -- E.logmsg TRACEZ (getpos ex) (text ("symWork: " ++ show (bound ++ sig.vars) ++ " " ++ nice ex g))
                        rhoz ← zonkRho sig.rho
                        let rho  = substRigidRho (bound ++ sig.vars) rhoz
                        expr  <- case expr of
                            Just dx  -> do
                                x <- dx
                                x <- zonkRigid (bound ++ sig.vars) x
                                return (Just (return x))
                            Nothing -> return Nothing
                        changeSym symv.{expr, typ = ForAll sig.bound rho}
        symWork _ = error "symWork: not a variable"

        zonk (x@Let {env,ex,typ = Just sigm}) = do
                let sig = substRigidSigma bound sigm
                syms <- mapSt U.findV env
                foreach syms symWork
                ex  <- zonkRigid bound ex
                stio (Right x.{ex,typ = Just sig})
        zonk (x@Lam {pat,ex,typ}) = do                  -- update also environment of lambda
            syms <- mapSt U.findV (map U.pVarLocal (patVars pat))
            foreach syms symWork
            case Expr.typ x of
                Just sigm -> do
                    let sigma = substRigidSigma bound sigm
                    stio (Left (x.{typ = Just sigma}))
                Nothing -> stio (Left x)
        zonk (Case {ckind,ex,alts,typ}) = do
            ex  <- zonkRigid bound ex
            typ <- case typ of
                Just sigma -> do
                    let s = substRigidSigma bound sigma
                    stio (Just s)
                Nothing -> stio Nothing
            alts <- mapSt zonkAlt alts
            stio (Right (Case ckind ex alts typ))
          where
            zonkAlt (CAlt {pat,ex}) = do
                syms <- mapSt U.findV (map U.pVarLocal (patVars pat))
                foreach syms symWork
                ex  <- zonkRigid bound ex
                stio (CAlt {pat,ex})
        zonk x = case Expr.typ x of
            Just sigm -> do
                let sigma = substRigidSigma bound sigm
                stio (Left (x.{typ = Just sigma}))
            Nothing -> stio (Left x)


zonkExpr x = mapEx false zonk x
    where
        zonk (x@Let {env,typ = Just sig}) = do
                sig <- zonkSigma sig
                syms <- mapSt U.findV env
                foreach syms symWork
                stio (Left x.{typ = Just sig})
            where
                symWork (symv@ SymV {pos, expr = Just dex, typ = sig}) = do
                        sig <- zonkSigma sig
                        ex <- dex
                        ex  <- zonkExpr ex
                        changeSym symv.{expr = Just (return ex), typ = sig}
                symWork _ = error "symWork: not a variable"
        zonk x
            | Just sig <- Expr.typ x = do
                sig <- zonkSigma sig
                stio (Left x.{typ=Just sig})
            | otherwise = do
                g <- getST
                E.fatal (getpos x) (text ("untyped expression  " ++ x.nice g))

approximate x = do
    rho <- approxRho x
    stio (ForAll [] rho)
approxRho :: Expr -> StG Rho
approxRho (Lam {ex,pat}) = do
    sig <- case pat of
        PAnn{pat, typ} -> return typ
        sonst          -> ForAll [] . RhoTau [] <$> newMeta2 ("arg", KType)
    rho <- approxRho ex
    stio (RhoFun [] sig rho)
approxRho _ = newRhoTyVar ("res", KType)


inferRho x = do
    rho    <- RhoTau [] <$> newMeta2 ("infer", KVar) -- doio (Ref.new Nothing)
    x      <- tcRho x (Infer rho)
    case x.typ of
        Just s -> return (s.rho, x)
        Nothing -> E.fatal (getpos x) (text "inferRho: no result")
checkRho x r = tcRho x (Check r)

checkSigma :: Expr -> Sigma -> StG Expr
checkSigma x s = checkSigma1 false x s
checkAnnotated x s = checkSigma1 true x s
checkSigma1 annotated x s = do
    (skolTvs, rho) <- skolemise s
    x <- checkRho x rho
    g <- getST
    let tvs = sigmaTvs g s
        eTvs = envTvs g 0
    let aTvs   = tvs ++ eTvs
        badTvs = [ tv | tv <- skolTvs, tv `elem` aTvs ]
        pos = getpos x

    let nicek g t = nice t g ++ "::" ++ show (MetaTv.kind t) 

    E.logmsg TRACET pos (text ("checkSigma1 " ++ show annotated ++ "  " ++ nice s g))
    E.logmsg TRACET pos (text ("skolTvs:  " ++ joined ", " (map (nicek g) skolTvs)))
    E.logmsg TRACET pos (text ("sigmaTvs: " ++ joined ", " (map (nicek g) tvs)))
    E.logmsg TRACET pos (text ("envTvs:   " ++ joined ", " (map (nicek g) eTvs)))
    E.logmsg TRACET pos (text ("badTvs: "   ++ joined ", " (map (nicek g) badTvs)))
    if null badTvs 
    then if annotated || not (null s.bound)
        then checkConstraints skolTvs x rho
        else -- this is justified by the fact that
             -- constraints could not introduce type variables
             -- that are not present in the type itself 
            return x
    else do
            let part1 = text "Type " <+> text (rho.nicer g)
                part2 = text "inferred from  " <+> text (x.nicer g) 
                part3 = text "is not as polymorphic as"
                        <+/> text "expected type " <+/> text (s.nicer g)
            E.error pos (part1 </> part2 </> part3)
            stio x
  where

        -- check constraints
        -- offered type must not be more constrained than expected in the skolemised ty vars
        checkConstraints tvs x expty = do
                x    <- resolveHas x
                ectx <- collectConstrs x
                let pos = getpos x
                let sigma = unJust (Expr.typ x)
                rho  <- simplify pos sigma.rho.{context=ectx}
                g    <- getST
                let rhometas = rhoTvs g rho.{context=[]}
                    ctxmetas = map (ctxTvs g) rho.context

                let fctx    = map snd . filter relevantCtx $ zip ctxmetas rho.context
                    -- onlyrho = filter (`notElem` tvs) rhometas -- only in rho, but not in skolTvs
                    relevantCtx
                        | annotated     = all (`elem` rhometas) 
                                            . filter (not . MetaTv.isFlexi)
                                            . fst 
                                            -- any (`elem`   rhometas) . fst
                        | otherwise     = any (`elem` tvs)
                                            -- . filter (not . MetaTv.isFlexi) 
                                            . fst

                    frho = rho.{context=fctx}
                x    <- return (x.{typ = Just sigma.{rho=frho}})                  
                let ety = canonicContext g expty

                E.logmsg TRACET pos (text ("expr context:     "   ++ nicectx fctx g))
                E.logmsg TRACET pos (text ("expected context: "   ++ nicectx ety.context g))
                -- find constraints that mention skolemised vars that are not in the expected type
                let implies = impliesG g
                    bad = [ ctx |   -- (ctx,ctvs) <- zip ectx etvss,
                                    -- annotated || any (`elem` tvs) ctvs,
                                    ctx  <- fctx,
                                    not (any (`implies` ctx) ety.context) ]

                    expected1 = if annotated then "annotated" 
                                             else "expected"
                    expected2 = if annotated then "annotated" else "expected "
                unless (null bad) do
                    g <- getST
                    let part1 = text ("Inferred type is more constrained than " ++ expected1 ++ " type.")
                        part2 = text "inferred " <+> text (nicer (betterReadable g (unJust x.typ)) g)
                        part3 = text expected2   <+> text (nicer s.rho g)
                    E.error (getpos x) (part1 </> part2 </> part3)
                    when (annotated) do
                        E.hint  (getpos x) (text "This could mean that your type signature is too general.")
                stio x


inferPat p = do
    sig    <- newSigmaTyVar ("inferpat", KType)
    binds  <- tcPat p (Infer sig)
    return sig

checkPat p s = tcPat p (Check s)

tcRho :: Expr -> Expected Rho -> StG Expr
tcRho x expty = case expty of
    Infer _  = do
        g <- getST
        E.logmsg TRACET (getpos x) (text ("tcRho Infer  " ++ x.nice g))
        tcRho' x expty
    Check t  = do
        g <- getST
        E.logmsg TRACET (getpos x) (text ("tcRho Check  " ++ x.nice g ++ "  for  " ++ t.nice g))
        tcRho' x expty


rhoFor s = RhoTau [] (TCon {pos=Position.null,name=TName pPreludeBase s})
rhoBool     = rhoFor "Bool" 
rhoChar     = rhoFor "Char" 
rhoString   = RhoTau [] tauString
rhoInt      = rhoFor "Int" 
rhoLong     = rhoFor "Long" 
rhoDouble   = rhoFor "Double" 
rhoFloat    = rhoFor "Float"
rhoDec      = RhoTau [] (TCon {pos=Position.null, name=TName pPreludeDecimal "Decimal"})
rhoRegex    = RhoTau [] (TCon {pos=Position.null, name=TName pUtilRegex "Regex"}) 
rhoMatcher  = RhoTau [] (TCon {pos=Position.null, name=TName pUtilRegex "MatchResult"})
rhoInteger  = rhoFor "Integer"
tauString   = TApp (tc "StringJ") (tc "Char")
numVar      = ForAll [tau] 
                     RhoTau{context=[Ctx{pos, cname=TName pPreludeBase "Num", tau}], tau}
                where tau = TVar{pos, kind=KType, var="int"}
                      pos = Position.null
realVar     = ForAll [tau] 
                     RhoTau{context=[Ctx{pos, cname=TName pPreludeBase "Real", tau}], tau}
                where tau = TVar{pos, kind=KType, var="int"}
                      pos = Position.null


instance Nice z => Nice (Maybe z) where
    nicer (Just x) g = x.nicer g
    nicer Nothing  g = "Nothing"
    nice x y = nicer x y


tcRho' :: Expr -> Expected Rho -> StG Expr

tcRho' (x@Lit {pos,kind, value})  ety = case kind of
    LBool   ->  instRho x (rhoBool) ety
    LChar   ->  instRho x (rhoChar) ety
    LString ->  instRho x (rhoString) ety
    LInt    ->  if isDWIM LInt value then do
                    r <- instantiate numVar
                    let t = maybe r Sigma.rho x.typ
                    instRho x  t  ety
                else instRho x (rhoInt) ety
    LLong   ->  instRho x (rhoLong)  ety
    LBig    ->  instRho x (rhoInteger)  ety
    LDouble ->  if isDWIM LDouble value then do
                    r <- instantiate realVar
                    let t = maybe r Sigma.rho x.typ
                    instRho x t ety
                else instRho x (rhoDouble)  ety
    LFloat  ->  instRho x (rhoFloat)  ety
    LDec    ->  instRho x rhoDec      ety
    LRegex  ->  instRho x (rhoRegex)  ety


tcRho' (x@Vbl{name}) (ety@Check erho)
    | higherRankedConstrainedArgs erho = do 
                            y ← expand x erho
                            tcRho y ety
    where
        higherRankedConstrainedArgs RhoFun{sigma, rho}
            | ForAll{bound, rho=r} ← sigma, not (null bound), not (null r.context) = true
            | otherwise = higherRankedConstrainedArgs rho
        higherRankedConstrainedArgs RhoTau{} = false
        expand ex RhoTau{} = pure ex
        expand ex RhoFun{rho} = do
            ex' <- expand ex rho
            pat ← U.freshVar x.pos
            pure Lam{pat, 
                        ex=App{fun=ex', 
                            arg=Vbl{pos=pat.pos, name=Local{uid=pat.uid, base=pat.var}, typ=Nothing}, 
                            typ=Nothing}, 
                        typ=Nothing} 
                
            
tcRho' (x@Vbl {name})  ety = do
    sym <- findVD name
    case sym of 
        SymD{} -> tcRho' Con{pos=x.pos, name=x.name, typ=x.typ} ety
        other  -> case isPSigma sym.typ of
            false -> if sym.state != Typechecked 
                    then do
                        sig ← fst <$> K.kiSigma [] [] sym.typ
                        changeSym sym.{typ=sig}
                        rho <- instantiate sig
                        instRho x rho ety 
                    else do
                        rho <- instantiate sym.typ
                        instRho x rho ety
                 
            true -> if sym.state == Unchecked
                then do
                    checkName name
                    sym <- findV name
                    rho <- instantiate sym.typ
                    instRho x rho ety
                else if sym.state == Typechecking
                     || sym.state == Recursive then do
                                -- unavoidable in mutual recursive definitions
                                changeSym sym.{state=Recursive}
                                rho <- approxRho x
                                instRho x rho ety
                          else do
                            g <- getST
                            E.fatal (getpos x) (text ("tcRho: untyped " ++ x.nice g ++ ", state=" ++ show sym.state))
tcRho' (x@Con {name}) ety = do
    sym <- U.findD name
    rho <- instantiate sym.typ
    instRho x rho ety

tcRho' (x@App a b t) ety = do
    (funty, fun)   <- inferRho a
    (argty, resty) <- unifyFun fun funty
    arg            <- checkSigma b argty
    instRho (App fun arg t) resty ety

tcRho' (x@Case {ex,alts}) ety
    | Infer _ <- ety  = do
        (rho,ex) <- inferRho ex
        (res,alt1) <- tcAlt rho (head alts)
        ralts <- mapSt (checkAlt rho (Check res)) (tail alts)
        instRho x.{ex,alts=alt1:ralts} res ety
    | Check crho <- ety = do
        (rho,ex) <- inferRho ex
        alts <- mapSt (checkAlt rho ety) alts
        let arho = (Sigma.rho . unJust • Expr.typ • CAlt.ex • head) alts
        instRho x.{ex, alts} arho ety
    where
        checkAlt rho ety (alt@CAlt {ex,pat})  = do
            (pat,ex) <- dwimPatEx pat ex
            checkPat pat (ForAll [] rho)
            ex <- tcRho ex ety
            stio alt.{pat,ex}
        tcAlt rho (alt@CAlt {ex,pat}) = do
            (pat,ex) <- dwimPatEx pat ex
            checkPat pat (ForAll [] rho)
            (rho, ex) <- inferRho ex
            stio (rho, alt.{pat, ex})

tcRho' (x@Let {env,ex}) ety = do
    g <- getST
    checkgroup env
    ex <- tcRho ex ety
    instSigma x.{env, ex} (unJust ex.typ) ety

tcRho' (lam@Lam {pat,ex}) (ety@Check rho) = do
        (pat, ex) <- dwimPatEx pat ex
        let x = lam.{pat, ex}
        (asig, brho) <- unifyFun x rho
        checkPat pat asig
        ex <- checkRho ex brho
        instRho x.{ex} (RhoFun [] asig (unJust ex.typ).rho) ety
tcRho' (lam@Lam {}) ety = do
    (pat, ex) <- dwimPatEx lam.pat lam.ex
    let x = lam.{pat, ex}
    sigma     <- inferPat x.pat
    (rho, ex) <- inferRho x.ex
    instRho (x.{ex}) (RhoFun [] sigma rho) ety

tcRho' (x@Mem {ex,member}) ety = do
        (rho, ex) <- inferRho ex
        g <- getST
        
        {-
        case ety  of
            Check RhoTau{tau=fun}
                | TApp a b <- reduced fun g,
                  TApp f _ <- reduced a g,
                  TCon{name=TName{base="->"}} <- reduced f g,
                  member.value.startsWith "upd$" || member.value.startsWith "chg$" -> do
                    let r = RhoTau [] b
                    ex <- checkRho ex r
                    return ((unJust ex.typ).rho, ex)
            _ -> inferRho ex
    
        -- (rho, ex) <- inferRho ex -}
        
        let pos = getpos x
        case rho of
            RhoFun _ _ _ -> do
                E.error pos (text ("primary expression  " ++ ex.nice g ++ "  must not be a function"))
                wrong <- newRhoTyVar ("wrong", KType)
                instRho x.{ex} wrong ety
            RhoTau _ taut -> do
                let tau = reducedTau g taut
                let expected ety
                        | Check RhoTau{tau=fun} <- ety,
                          TApp a b <- reduced fun g,
                          TApp f _ <- reduced a g,
                          TCon{name=TName{pack,base="->"}} <- reduced f g,
                          pack == pPreludeBase,
                          member.value.startsWith "upd$" || member.value.startsWith "chg$"
                        = [reducedTau g b]
                        | otherwise = []
                tcMem pos ex member (tau:expected ety) ety
    where
        tcMem :: Position -> Expr -> Token -> [Tau] -> Expected Rho -> StG Expr
        tcMem pos ex member [] ety = do
            resolveme <- newRhoTyVar ("unresolved", KType)
            instRho Mem{ex, member, typ=Nothing} resolveme ety
        tcMem pos ex member (tau:taus) ety = do
            g <- getST
            -- let etytxt = 
            E.logmsg TRACET pos (text "tcMem"
                <+> nicest g ex <+> text member.value <+> PP.sep "," (map (text . flip nice g) (tau:taus))
                <+> case ety of 
                        Check t -> text "Check" <+> text (nice t g)
                        Infer t -> text "Infer" <+> text (nice t g)
                )
            let mpos = Pos member member
                original = if member.value.startsWith "upd$"
                                || member.value.startsWith "chg$" 
                            then member.{value <- flip strtail 4}
                            else member
                     
            case instTauSym tau g of
                Just (SymT {name, env, nativ, newt})
                    | Just (SymV {name}) <- env.lookup member.value = do
                            changeST Global.{sub <- SubSt.{
                                idKind <- insert (KeyTk original) (Right name)}}
                            weUse name
                            tcRho (nApp (Vbl mpos name Nothing) ex) ety
                    | Just (SymL {alias}) <- env.lookup member.value = do
                            changeST Global.{sub <- SubSt.{
                                idKind <- insert (KeyTk original) (Right alias)}}
                            weUse alias
                            tcRho (nApp (Vbl mpos alias Nothing) ex) ety
                    | Just s <- nativ,          -- it's a native type
                      -- traceLn ("nativ " ++ s) || true,
                      ss <- s:U.supersOfNativ s g,     -- the supertypes of s (including s)
                      -- traceLn ("supers " ++ show ss) || true,
                      qns <- [ q | s <- ss, q <- U.typesOfNativ s g ],
                      -- traceLn ("types " ++ show qns) || true,
                      h:_ <- [ h | q <- qns, h <- g.findit (MName q member.value) ] = do
                            let m = case h of
                                        SymV {name}  -> name
                                        SymL {alias} -> alias
                                        _ -> error "no symbol or alias"
                            changeST Global.{sub <- SubSt.{
                                idKind <- insert (KeyTk original) (Right m)}}
                            weUse m
                            tcRho (nApp (Vbl mpos m Nothing) ex) ety
                    | newt,
                      name == TName pPreludeIO "Mutable",   -- it is some Mutable type
                      TApp _ ntau <- tau,                   -- Mutable x ntau
                      TCon{name=tcon}:_ <- ntau.flat,
                      Just SymT{nativ=Just s} <- g.findit tcon,
                      SymV{name=m}:_ <- [ h | sup <- s:U.supersOfNativ s g, 
                                                q <- U.typesOfNativ sup g,
                                                h <- g.findit (MName q member.value) ]                    
                      = do
                            changeST Global.{sub <- SubSt.{
                                idKind <- insert (KeyTk original) (Right m)}}
                            weUse m
                            tcRho (nApp (Vbl mpos m Nothing) ex) ety
                other | Just (m@SymV {name=MName clas _}) <- g.findit (VName g.thisPack member.value),
                        Just (SymC {tau}) <- g.findit clas = do
                            changeST Global.{sub <- SubSt.{
                                idKind <- insert (KeyTk original) (Right m.name)}}
                            weUse m.name
                            tcRho (nApp (Vbl mpos m.name Nothing) ex) ety
                sonst -> tcMem pos ex member taus ety

tcRho' (x@Ifte a b c _) (ety@Infer _) = do
    a <- checkRho a (rhoBool)
    (r,b) <- inferRho b
    c <- checkRho c r
    instRho (Ifte a b c Nothing) r ety

tcRho' (x@Ifte a b c _) (ety@Check erho) = do
    a <- checkRho a (rhoBool)
    b <- checkRho b erho
    let trho = Sigma.rho (unJust b.typ)
    c <- checkRho c trho
    instRho (Ifte a b c Nothing) trho ety

tcRho' (x@Ann ex (Just s)) ety  = do         -- a genuine forall, should be rare
    sig ← fst <$> K.kiSigma [] [] s
    ex <- checkAnnotated ex sig
    instSigma ex sig ety
    -- instSigma ex (unJust ex.typ) ety         -- we don't want to see Ann after typechecking anymore

tcRho' x (Check _) = do
    g <- getST
    E.fatal (getpos x) (text ("can't tcRho (check): " ++ x.nice g))
tcRho' x (Infer _) = do
    g <- getST
    E.fatal (getpos x) (text ("can't tcRho (infer): " ++ x.nice g))


tcPat p expty = case expty of
    Infer _  = do
        g <- getST
        E.logmsg TRACET (getpos p) (text ("tcPat Infer  " ++ p.nice g))
        tcPat' p expty
    Check s  = do
        g <- getST
        E.logmsg TRACET (getpos p) (text ("tcPat Check  " ++ p.nice g ++ "  for  " ++ s.nice g))
        tcPat' p expty

sigFor s   = ForAll [] (RhoTau [] (TCon {pos=Position.null,name=TName pPreludeBase s}))
sigBool    = ForAll [] rhoBool
sigChar    = ForAll [] rhoChar
sigString  = ForAll [] rhoString
sigInt     = ForAll [] rhoInt
sigLong    = ForAll [] rhoLong
sigInteger = ForAll [] rhoInteger
sigDouble  = ForAll [] rhoDouble
sigFloat   = ForAll [] rhoFloat
sigDec     = ForAll [] rhoDec
sigRegex   = ForAll [] rhoRegex
sigMatcher = ForAll [] rhoMatcher

litSigma LBool      = sigBool
litSigma LChar      = sigChar
litSigma LString    = sigString
litSigma LInt       = sigInt
litSigma LLong      = sigLong
litSigma LBig       = sigInteger
litSigma LDouble    = sigDouble
litSigma LFloat     = sigFloat
litSigma LDec       = sigDec
litSigma LRegex     = sigRegex

tcPat' (p@PLit {pos,kind})  ety = case kind of
    LBool   -> instPatSigma p (sigBool) ety
    LChar   -> instPatSigma p (sigChar) ety
    LString -> instPatSigma p (sigString) ety
    LInt    -> instPatSigma p (sigInt)  ety
    LLong   -> instPatSigma p (sigLong)  ety
    LBig    -> instPatSigma p (sigInteger) ety
    LDouble -> instPatSigma p (sigDouble) ety
    LFloat  -> instPatSigma p (sigFloat) ety
    LDec    -> instPatSigma p sigDec ety
    LRegex  -> instPatSigma p (sigString) ety

tcPat' (p@PVar {uid,var}) (ety@Check sig) = do
    sym <- findV (Local{uid, base=var})
    -- E.logmsg TRACET p.pos (text("lookup PVar{uid=" ++ show uid ++ "} --> " ++ show sym.name))
    case isPSigma sym.typ of
        true  -> do  changeSym sym.{typ=sig, state=Typechecked}
                     instPatSigma p sig ety
        false -> instPatSigma p sym.typ ety

tcPat' (p@PVar {uid,var}) ety = do
    sym <- findV (Local{uid, base=var})
    -- E.logmsg TRACET p.pos (text("lookup PVar{uid=" ++ show uid ++ "} --> " ++ show sym.name))
    case isPSigma sym.typ of
        true -> do
            sig <- newSigmaTyVar (var, KType)
            changeSym sym.{typ = sig, state = Typechecked}
            instPatSigma p sig ety
        false -> instPatSigma p sym.typ ety

tcPat' (p@PMat {pos,uid,var}) ety = do
    checkPat (PVar {pos,uid,var}) sigMatcher
    instPatSigma p sigString ety

tcPat' (p@PCon {qname,pats}) ety = do
    sym <- findD qname
    rho <- instantiate sym.typ
    let spRho (RhoFun _ s r) = case spRho r of
            (args, ret) -> (s:args,ret)
        spRho rhotau = ([], rhotau)
    case spRho rho of
        (!sigs, !res) = do
            mapSt (\(p,s) -> checkPat p s) (zip pats sigs)
            instPatSigma p (ForAll [] res) ety

tcPat' (p@PAnn {pat,typ}) ety = do
    sig ← fst <$> K.kiSigma [] [] typ
    checkPat pat sig
    instPatSigma p sig ety

tcPat' (p@PUser {pat}) ety = tcPat' pat ety

tcPat' (p@PAt {pos,uid,var,pat}) (ety@Infer _) = do
    sig <- inferPat pat
    checkPat (PVar {pos,uid,var}) sig
    instPatSigma p sig ety
tcPat' (p@PAt {pos,uid,var,pat}) (ety@Check sig) = do
    checkPat pat sig
    checkPat (PVar {pos,uid,var}) sig
    instPatSigma p sig ety

tcPat' p _ = do
    g <- getST
    E.fatal (getpos p) (text ("can't tcPat:  " ++ p.nice g))

private real = TName{pack=pPreludeBase, base="Real"}
private num  = TName{pack=pPreludeBase, base="Num"}

--- Type the literals
--- Make sure all constraints are removed when a type is found
literalType ctxs (lit@Lit{pos, kind, value, typ=Just sigma})
    | kind != LInt, kind != LDouble = return (Left lit)
    | kind == LInt, isDWIM LInt value, RhoTau _ taut <- sigma.rho = do
            
            g <- getST
            let tau = reduced taut g
                
            
            case tau of
                TCon{pos, name}
                    | name == rhoInt.tau.name     = strip lit
                    | name == rhoLong.tau.name    = strip lit.{kind=LLong, value <- (++"L")}
                    | name == rhoInteger.tau.name = strip lit.{kind=LBig}
                    | name == rhoFloat.tau.name   = strip lit.{kind=LFloat, value <- (++"F")}
                    | name == rhoDouble.tau.name  = strip lit.{kind=LDouble, value <- (++"D")}
                    | otherwise = fromInt
                Meta Flexi{uid, hint, kind}  = do  -- unbound, because already reduced
                        
                        let rctxs = reducedCtxs g ctxs
                        let qns = [ cname | 
                                    Ctx{pos, cname, tau = Meta Flexi{uid=id}} <- rctxs, 
                                    uid == id ] 
                        if (real `elem` qns
                            ||  TName{pack=pPreludeMath, base="Floating"} `elem` qns
                            ||  any (U.isSuper real g) qns)
                        then instRho lit.{kind=LDouble, value <- (++"D")} sigma.rho (Check rhoDouble)
                                >>= strip       -- infer Double
                        else checkRho lit rhoInt
                                >>= strip       -- infer Int
                Meta Rigid{} -> fromInt
                TApp _ _     -> fromInt             -- force type error unless Num             
                _            -> do
                    x <- checkRho lit rhoInt        -- fix unresolved to Int
                    strip x                         -- or force type error
    | kind == LDouble, isDWIM LDouble value, RhoTau _ taut <- sigma.rho = do
            g <- getST
            let tau = reduced taut g
            
            case tau of
                TCon{pos, name}
                    | name == rhoFloat.tau.name   = strip lit.{kind=LFloat, value <- (++"F")}
                    | name == rhoDouble.tau.name  = strip lit.{kind=LDouble, value <- (++"D")}
                    | otherwise = fromDouble
                Meta Rigid{} -> fromDouble
                TApp _ _     -> fromDouble          -- force type error unless Real             
                _            -> do
                    x <- checkRho lit rhoDouble     -- fix unresolved to Double
                    strip x                         -- or force type error
    | kind == LDouble = checkRho lit rhoDouble >>= strip   -- no DWIM
    | otherwise       = checkRho lit rhoInt    >>= strip   -- no DWIM
    where
        strip ∷ ExprT → StG (ExprT | ExprT)
        strip x = pure . Right $ x.{typ ← fmap _.{rho ← _.{context = []}}}
        frmIntlit = nApp frmInt lit.{typ=Just sigInt}
        frmDbllit = nApp frmDbl lit.{typ=Just sigDouble}
        frmInt = Vbl{pos = pos.change VARID "fromInt", 
                     name = MName{tynm=num, base="fromInt"}, typ=Nothing}
        frmDbl = Vbl{pos= pos.change VARID "fromDouble",
                     name = MName{tynm=real, base="fromDouble"}, typ=Nothing}
        fromInt    = checkRho frmIntlit sigma.rho.{context=[]} >>= strip
        fromDouble = checkRho frmDbllit sigma.rho.{context=[]} >>= strip
literalType _ x = return (Left x)


--- Resolve the x.m finally
--- Resolve overloaded methods
resolveHas ∷ ExprT → ExprD Global
resolveHas expr = do
        ctxs  <- collectConstrs expr
        mems  <- foldEx true countMem 0 expr    -- count how many mems we have
        mapEx true (literalType ctxs) expr >>= resolveHas' mems
    where
        resolveHas' ∷ Int → ExprT → ExprD Global
        resolveHas' 0 ex = mapEx true (rHas true) ex
        resolveHas' n ex = do
            E.logmsg TRACET (getpos ex) (text("TDNR for  " ++ show n ++ " expressions"))
            nex <- mapEx  true (rHas false) ex
            m   <- foldEx true  countMem 0 nex
            if m < n        -- something has been resolved
            then resolveHas' m nex
            else resolveHas' 0 nex  -- finish with error messages
        -- count number of Mem constructs plus overloaded vars 
        countMem ∷ Int → ExprT → StG (Int | Int)
        countMem !acc Mem{}  = return . Left $! (acc+1)
        countMem !acc Vbl{name} 
            | not name.isLocal    =  do
                    sym <- U.findV name
                    case sym.over of
                        [] ->  return . Right $! acc            -- not overloaded
                        _  ->  return . Right $! (acc+1)        -- overloaded
        countMem !acc _      = return . Left $! acc
        
--- try to resolve an overloaded name or a member expression
--- the first argument tells if we flag errors or not
rHas ∷ Bool → ExprT → StG (ExprT | ExprT)
rHas flagerr (x@Mem{ex, member, typ = Just sigma}) = do
    g ← getST
    E.logmsg TRACET (getpos x) (text "[TDNR" <+> text (show flagerr) <> text "]" 
        <+> nicest g x )
    app <- checkRho x.{typ = Nothing} sigma.rho -- now type of ex should be known
    case app of
        Mem{}
            | not flagerr = return (Left x)
            | Just sigma <- ex.typ,
              RhoTau{tau=taut} <- sigma.rho = do
                g <- getST 
                let tau = reduced taut g
                case tau.flat of
                    TCon{}:_   = do
                        E.error (getpos x) (text "can't find a type for " 
                            <+/> text (x.nicer g)
                            <+/> text "`" <> text member.value <> text "`"
                            <+/> text "is neither an overloaded function nor a member of "
                            <+/> text (sigma.rho.nicer g))
                        return (Left x)
                    unknown = badsigma sigma
            | Just sigma <- ex.typ = badsigma sigma
            | otherwise = badsigma pSigma
            where
                badsigma sigma =  do
                        g <- getST 
                        E.error (getpos x) (text "can't find a type for " 
                            <+/> text (x.nicer g) 
                            <+/> text " because " 
                            <+/> (text (ex.nicer g)
                                    <+> text "::" 
                                    <+> text (nicer sigma g))
                            <+/> text " does not have a definite type.")
                        return (Left x)
        other -> return (Left app)      -- Mem resolved (or not flagged)

rHas _ (x@Mem{ex, member, typ = Nothing}) = do
    g <- getST
    error ("expression  " ++ x.nicer g ++ "  is untyped")

rHas flagerr (v@Vbl{pos, name, typ}) | not name.isLocal = do
        sym <- U.findV name
        case sym.over of
            [] -> return (Right v)
            _  -> resolveOver v sym
    where
        -- resolve overloaded variable
        resolveOver :: Expr -> Symbol -> StG (Expr|Expr)
        resolveOver v sym = do
                g <- getST
                let sigma = (unJust v.typ)
                E.logmsg TRACET v.pos (text ("resolve overloaded " ++ nice v.name g 
                                            ++ " :: " ++ nice sigma g))
                                                    
                let candidates = overloads g sym
                    groups 
                        | MName{} <- sym.name = groupBy (using (QName.tynm . Symbol.name)) candidates
                        | otherwise = [candidates]
                
                E.logmsg TRACET v.pos (text ("by " 
                    ++ joined ", " (map (flip nice g . Symbol.name) candidates)))
                    
                checked <- mapM (resolve v.pos sigma) groups
                case filter (not . null) checked of
                    [] | not flagerr = do
                        E.logmsg TRACET v.pos (text "overloaded " <+> text (nicer v g) 
                            <+> text " cannot yet be resolved at type "
                            <+/> text (nicer sigma g))
                        return (Right v)
                    [] -> do
                        E.error v.pos (text "overloaded " <+> text (nicer v g) 
                            <+> text " cannot be resolved at type "
                            <+/> text (nicer sigma g))
                        return (Right v)
                    ms:_ -> case sortBy (comparing arity) ms of                     -- compare b arity to find 
                                                                                    --       the one that fits
                        cs  → case filter ((arity (head cs) ==) . arity) cs of      -- remove the ones that don't
                            some -> do
                                when (length some > 1) do
                                    E.warn v.pos (text "overloaded `" <> text (nicer v g) 
                                        <>  text "´ is ambiguous at type "
                                        <+/> text (nicer sigma g)
                                        </>  text "It could mean one of "
                                        </>  stack [ text (nicer (Symbol.name s) g) 
                                                        <+> text " :: " 
                                                        <+> text (nicer s.typ g)
                                                | s <- some ]) 
                                let s = head some
                                    diag = if length some > 1 then E.warn else E.explain
                                diag v.pos (msgdoc ("overloaded " ++ nicer v.name g 
                                                ++ " :: " ++ nicer sigma g
                                                ++ "  resolved to  "
                                                ++ nicer s.name g))
                                x <- checkSigma Vbl{pos=v.pos, name=s.name, typ=Nothing} sigma
                                changeST Global.{sub <- SubSt.{
                                            idKind <- insert (KeyTk v.pos.first) (Right s.name)}}
                                return (Right x)
            where
                resolve ∷ Position → Sigma → [Symbol] → StG [Symbol]
                resolve pos sigma [] = return []
                resolve pos sigma (sym:syms) = do
                    g1 <- getST
                    changeST Global.{options <- Options.{flags <- flagSet OVERLOADING}}
                    x <- checkSigma Vbl{pos, name=Symbol.name sym, typ=Nothing} sigma
                    g <- getST
                    putST g1
                    if (g.errors > g1.errors)
                    then resolve pos sigma syms
                    else do
                        rs <- resolve pos sigma syms
                        return (sym:rs)
                overloads ∷ Global → Symbol → [Symbol]
                overloads g sym = case sym of
                    SymV{over=[]} -> [sym]
                    SymV{pos, name = MName{tynm, base}, over=(_:_)}
                        | Just SymT{nativ = Just this} <- g.findit tynm,
                          ov <- [ sy | m <- sym.over, sy <- g.findit m ],
                          syms <- [ sy | s  <- U.supersOfNativ this g, 
                                         q  <- U.typesOfNativ s g, 
                                         h  <- g.findit (MName q base),
                                         sy <- overloads g h] 
                        = ov++syms
                    SymV{} -> [ sy | m <- sym.over, sy <- g.findit m]
                    _ -> []

rHas _ x = pure (Left x)             

--- collect all class constraints
collectConstrs = U.foldEx true collC []
    where
        collC cxs x = case Expr.typ x of
            Just sigma -> getST >>= (return . Left . flip mergeCtx cxs . flip reducedCtxs cs)
                            where cs = map Context.{pos=getpos x} sigma.rho.context 
            Nothing    -> return (Left cxs)  
            


--- Inform about unused imports.             
unusedImports = do
    -- inform abóut unused packages
    g <- getST
    -- E.logmsg TRACET Position.null (text("name spaces used: " ++ show (keys g.sub.nsUsed)))
    -- E.logmsg TRACET Position.null (text("packsWhy: " ++ show (each g.sub.packWhy)))
    let unused = [ (n,p, pos) | (n,p) <- each g.namespaces,
                    not (g.sub.nsUsed `contains` n),
                    not (p `elem` map fst preludePacks),
                    p != pPrelude, p != g.thisPack,
                    pos = fromMaybe Position.null (g.sub.nsPos.lookup n) ]
        notused (n,p,pos) = E.hint pos (msgdoc("unused import of  "
                ++ (unmagicPack p.raw) ++ "  as  " ++ n.unNS))
    foreach unused notused
               
